#include <stdio.h>
#include <stdarg.h>
#include <sizes.h>

int fputc(int c, FILE *f)
{
    uint8_t ch = c & 0xFF;

    if (__stdio_write(f, &ch, 1) < 0)
        return EOF;
    return ch;
}